(declare-fun a () Real)
(declare-fun b () Real)
(declare-fun c () Real)
(declare-fun aa () Real)
(declare-fun ab () Real)
(declare-fun d () Real)
(declare-fun e () Real)
(declare-fun f () Real)
(declare-fun j () Real)
(declare-fun g () Real)
(declare-fun i () Real)
(declare-fun h () Real)
(declare-fun k () Real)
(declare-fun ad () Real)
(declare-fun ag () Real)
(assert (not (exists ((ai Real)) (=> (>= 0 c) (=> (<= 0 e) (or (> 0 ai) (> 0 (+ (* (+ b g) ai) aa)) (> (+ ai aa) (- i d))))))))
(assert (not (exists ((aj Real)) (= (and (or (and (= (+ b e) (+ a f)) (<= f b)) (<= 0 ad)) (= (- d i) 2) (< (+ ab (/ 0 (/ 2 k))) 0 k e a)) (or (< (/ 1 c) (* 2 (/ (- 1) k))) (< (/ (* (+ (* k (- f b)) ad) (+ (* (/ (- 1) k) (- b f)) ad)) (* 2 k)) 0))))))
(assert (= b (+ f h)))
(assert (= c (+ j ag) (+ g h)))
(check-sat)
